Step of Proof: outr_wf
12,41
postcript
pdf
Inference at
*
1
I
of proof for Lemma
outr
wf
:
1.
A
: Type
2.
B
: Type
3.
x
:
A
+
B
4.
(
isl(
x
))
outr(
x
)
B
latex
by ((D 3)
CollapseTHENM (Reduce (-1)))
latex
C
1
:
C1:
3.
x1
:
A
C1:
4. False
C1:
outr(inl
x1
)
B
C
2
:
C2:
3.
y
:
B
C2:
4. True
C2:
outr(inr
y
)
B
C
.
Definitions
if
b
then
t
else
f
fi
,
ff
,
tt
,
isl(
x
)
,
b
,
b
origin